Software testing is often a difficult aspect of software development. One tool for testing, model checking, can use state exploration for detecting bugs, such as data races, and for verifying that a model or implementation satisfies given temporal properties. State exploration can be particularly effective when a symbolic state representation is used, as this can allow multiple concrete state instances to be represented by one symbolic state.
Constraint solvers used in symbolic state exploration, such as “sat-solvers,” can check whether a solution for a symbolic state exists, but cannot enumerate all possible solutions, as is often required. However, given a finite domain over-approximation of symbolic terms (which may themselves include several symbolic terms) used in a symbolic state, the problem of enumerating solutions can be reduced to a satisfiability problem, which is feasible for sat-solvers using finite domain constraint resolution techniques.